/* ==============================================================================
*
*   Copyright (c) 2010, Pierre Favier
*   All rights reserved.
*
*   NTasking is free software: you can redistribute it and/or modify it
*   under the terms of the GNU General Public License as published by the
*   Free Software Foundation.
*
*   Redistribution and use in source and binary forms, with or without
*   modification, are permitted provided that the following conditions
*   are met:
*
*   -   Redistributions of source code must retain the above copyright notice,
*       this list of conditions and the following disclaimer.
*
*   -   Redistributions in binary form must reproduce the above
*       copyright notice, this list of conditions and the following
*       disclaimer in the documentation and/or other materials
*       provided with the distribution.
*
*   THIS SOFTWARE IS PROVIDED "AS IS" AND ANY EXPRESS OR IMPLIED
*   WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
*   OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
*   DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS
*   BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
*   EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
*   TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
*   DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
*   ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR
*   TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF
*   THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
*   SUCH DAMAGE.
*
* ============================================================================== */

using System;
using NTasking.ValidationTests.ACATS_3_0.Support;
using NUnit.Framework;
using Rhino.Mocks;

namespace NTasking.ValidationTests.ACATS_3_0.C9
{
    [TestFixture(Description = "")]
    public class C940A03 : ValidationTest
    {

        // Declare a resource descriptor tagged type.  Extend the type and
        // use the extended type in a protected data structure.
        // Implement a counting semaphore type that can be initialized to a 
        // specific number of available resources.  Declare an entry for 
        // requesting a specific resource and an procedure for releasing the 
        // same resource it.  Declare an object of this (protected) type, 
        // initialized to two resources.  Declare and start three tasks each 
        // of which asks for a resource.  Verify that only two resources are 
        // granted and that the last task in is queued.
        //
        // This test models a multi-user operating system that allows a limited
        // number of logins.  Users requesting login are modeled by tasks.


        const int MaxLogins = 2;

        const int InitKey = 0;


        private static LoginSemaphore loginSemaphore;
        private static Counter counter;
        private static Interlock tcControlMessage;


        private class Resource
        {

            internal int Id { get; set; }


            internal Resource()
            {
                Id = 0;
            }

        }


        private class LoginRecord : Resource
        {

            internal int Key { get; set; }


            internal LoginRecord()
            {
                Key = InitKey;
            }

        }


        private class LoginSemaphore : Protected
        {

            private int LoginsAvail;
            private int NextKey = InitKey;


            [Entry]
            internal Func<LoginRecord, LoginRecord> RequestLogin { get; private set; }

            [ReadWriteOperation]
            internal Action ReleaseLogin { get; private set; }

            [ReadOnlyOperation]
            internal Func<int> Available { get; private set; }


            internal LoginSemaphore(int resourcesAvailable)
            {
                LoginsAvail = resourcesAvailable;

                Entry(RequestLogin,
                    When: () => LoginsAvail > 0,
                Is: resourceKey =>
                {
                    LoginRecord result = resourceKey;

                    NextKey += 1;
                    result.Key = NextKey;
                    LoginsAvail -= 1;

                    return result;
                });

                ReadWriteOperation(ReleaseLogin, Is: () =>
                {
                    LoginsAvail += 1;
                });

                ReadOnlyOperation(Available, Is: () =>
                {
                    return LoginsAvail;
                });
            }

        }


        private class UserTask : ValidationTestTask
        {

            [Entry]
            internal Action<int> Login { get; private set; }

            [Entry]
            internal Action Logout { get; private set; }

            [Entry]
            internal Func<LoginRecord> GetStatus { get; private set; }


            internal UserTask(IValidationTestResult result)
                : base(result)
            {
            }


            protected override void Body()
            {
                LoginRecord rec = new LoginRecord();
                bool finished = false;

                while (!finished)
                {
                    Select(s => s.

                        Accept(Login, (id) =>
                        {
                            rec.Id = id;
                        }).
                        Then(() =>
                        {
                            // request a resource; if resource is not available, 
                            // task will be queued to wait
                            rec = loginSemaphore.RequestLogin(rec);

                            counter.Increment();
                            // after resource is obtained, post message
                            tcControlMessage.Post();
                        }).

                    Or.

                        Accept(Logout, () =>
                        {
                            loginSemaphore.ReleaseLogin();
                            counter.Decrement();
                        }).
                        Then(() =>
                        {
                            finished = true;
                        }).

                    Or.

                        Accept(GetStatus, () =>
                        {
                            return rec;
                        })
                    );
                }
            }
            protected override void Exception(Exception ex)
            {
                Console.WriteLine("Exception raised in model user task");
                Result.TestFailed();
            }
        }


        private static int TCKeyVal(LoginRecord loginRec)
        {
            return loginRec.Key;
        }


        [Test(Description =
            "Check that a protected object provides coordinated access to " +
            "shared data.  Check that it can implement a semaphore-like construct " +
            "controlling access to shared data through procedure parameters to " +
            "allow a specific maximum number of tasks to run and exclude all " +
            "others.")]
        public void Test()
        {
            IValidationTestResult result = Mocks.DynamicMock<IValidationTestResult>();
            UserTask task1 = null;
            UserTask task2 = null;
            UserTask task3 = null;
            LoginRecord userRec;

            Ada.Declare(() =>
            {
                counter = new Counter();
                tcControlMessage = new Interlock();
                loginSemaphore = new LoginSemaphore(MaxLogins);
                task1 = new UserTask(result);
                task1.Name = "1";
                task2 = new UserTask(result);
                task2.Name = "2";
                task3 = new UserTask(result);
                task3.Name = "3";

                // Setup text expectations

                Expect.Call(() => result.TestFailed()).Repeat.Never();
                Expect.Call(() => result.TaskFinished(task1));
                Expect.Call(() => result.TaskFinished(task2));
                Expect.Call(() => result.TaskFinished(task3));

                Mocks.ReplayAll();
            },
            Begin: () =>
            {
                if (counter.Number() != 0)
                {
                    Console.WriteLine("Wrong initial conditions");
                    result.TestFailed();
                }

                task1.Login(1); // request resource; request should be granted
                tcControlMessage.Consume();
                                // ensure that task obtains resource by
                                // waiting for task to post message

                                // Task 1 waiting for call to Logout
                                // Others still available

                userRec = task1.GetStatus();

                if (counter.Number() != 1 ||
                    loginSemaphore.Available() != 1 ||
                    TCKeyVal(userRec) != 1)
                {
                    Console.WriteLine("Resource not assigned to task 1");
                    result.TestFailed();
                }

                task2.Login(2); // request resource; request should be granted
                tcControlMessage.Consume();
                                // ensure that task obtains resource by
                                // waiting for task to post message

                userRec = task2.GetStatus();

                if (counter.Number() != 2 ||
                    loginSemaphore.Available() != 0 ||
                    TCKeyVal(userRec) != 2)
                {
                    Console.WriteLine("Resource not assigned to task 2");
                    result.TestFailed();
                }

                task3.Login(3); // request for resource should be denied
                                // and task queued

                                // Tasks 1 and 2 holds resources
                                // and are waiting for a call to Logout
                                // Task 3 is queued

                if (counter.Number() != 2 ||
                    loginSemaphore.Available() != 0)
                {
                    Console.WriteLine("Resource incorrectly assigned to task 3");
                    result.TestFailed();
                }

                task1.Logout(); // -- released resource should be given to
                                // queued task
                tcControlMessage.Consume();
                                // wait for confirming message from task

                                // Task 1 holds no resources
                                //   and is terminated (or will soon)
                                // Tasks 2 and 3 hold resources
                                //   and are waiting for a call to Logout

                userRec = task3.GetStatus();
                if (counter.Number() != 2 ||
                    loginSemaphore.Available() != 0 ||
                    TCKeyVal(userRec) != 3)
                {
                    Console.WriteLine("Resource not properly released/assigned to task 3");
                    result.TestFailed();
                }

                task2.Logout(); // no outstanding request for released
                                // resource
                                // Tasks 1 and 2 hold no resources
                                // Task 3 holds a resource
                                // and is waiting for a call to Logout

                if (counter.Number() != 1 ||
                    loginSemaphore.Available() != 1)
                {
                    Console.WriteLine("Resource not properly released from task 2");
                    result.TestFailed();
                }

                task3.Logout(); // all resources have been returned
                                // all tasks have terminated or will soon

                if (counter.Number() != 0 ||
                    loginSemaphore.Available() != 2)
                {
                    Console.WriteLine("Resource not properly released from task 3");
                    result.TestFailed();
                }

                while (!task1.Terminated &&
                       !task2.Terminated &&
                       !task3.Terminated)
                    Ada.Delay(Impdef.MinimumTaskSwitch);
            });
        }

    }

}
